
def main():
    x = 0
    while True:
        x:int = nondet_int()
        if x == 0:
            x = 3
        elif x == 1:
            x = 2
        elif x == 2:
            assert x >= 2
            x = 3
        else:
            # 如果x不是0, 1, 或2，则退出循环
            break
    
    assert x == 3

# 调用main函数
main()
